Here we show that reduction preserves the well typedness of processes, to this aim we need three auxiliary lemmata. The first one handles substitutions.

\begin{lemma}[Substitution]\label{lem:substitution}
\begin{enumerate}
 \item If $\env{\Gamma}{ \Theta} \vdash P:\type{\Phi}{\Delta}$ then $\env{\Gamma}{ \Theta} \vdash P\sub{c'}{c}:\type{\Phi\sub{c'}{c}}{\Delta}$. 
  \item If $\env{\Gamma}{ \Theta} \vdash P:\type{\Phi}{\Delta}$ then $\env{\Gamma}{ \Theta} \vdash P\sub{\tilde{e}}{\tilde{x}}:\type{\Phi}{\Delta}$. 

  \item If $\judgebis{\env{\Gamma}{ \Theta,X:\type{\Phi'}{\Delta'}}}{P}{\type{\Phi}{\Delta}}$ and $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\Phi'}{\Delta'}}$ then $\judgement{\Gamma}{\Theta}{P\sub{Q}{X}}{\Phi}{\Delta}$.
   \item If $\judgebis{\env{\Gamma}{ \Theta,\mathsf{X}:\Delta'}}{P}{\type{\Phi}{\Delta}}$ and $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\Phi'}{\Delta'}}$ then $\judgement{\Gamma}{\Theta}{P\sub{Q}{\mathsf{X}}}{\Phi}{\Delta}$.
\end{enumerate}
\end{lemma}



The second lemma allows to reverse typing rules and it follows from the definition of the typing system.
\begin{lemma} \label{lem:types} \quad \\
\begin{enumerate}
 \item \label{types1} if $\judgement{\Gamma}{\Theta}{P \parallel Q}{\Phi}{\Delta}$ then there exists $\Phi_1, \Phi_2, \Delta_1, \Delta_2$  such that $\judgement{\Gamma}{\Theta}{P}{\Phi_1}{\Delta_1}$,  $\judgement{\Gamma}{\Theta}{Q}{\Phi_2}{\Delta_2}$, $\Phi= \Phi_1 \bowtie  \Phi_2$ and $\Delta = \Delta_1 \uplus \Delta_2$;
 \item \label{types2} if $\judgement{\Gamma}{\Theta}{\inC{c}{\tilde{x}}.P}{\Phi}{\Delta}$ then there exists $\rho$  such that $\Phi = \Phi', c:?(\tilde{\kappa}).\rho $ and  $\judgement{\Gamma, \tilde{x}:\tilde{\kappa}}{\Theta}{P}{\Phi', c:\rho}{\Delta}$;
 \item \label{types3} if $\judgement{\Gamma}{\Theta}{\outC{c}{\tilde{e}}.P}{\Phi}{\Delta}$ then there exists $\rho$  such that $\Phi = \Phi', c:!(\tilde{\kappa}).\rho $ and  $\judgement{\Gamma}{\Theta}{P}{\Phi', c:\rho}{\Delta}$;

 \item \label{typesdelin} if $\judgement{\Gamma}{\Theta}{\catch{c}{d}.P}{\Phi}{\Delta}$ then there exist $\rho, \sigma$  such that $\Phi = \Phi', c:?(\sigma).\rho $ and  $\judgement{\Gamma}{\Theta}{P}{\Phi', c:\rho, d:\sigma}{\Delta}$;
 \item \label{typesdelout} if $\judgement{\Gamma}{\Theta}{\throw{c}{d}.P}{\Phi}{\Delta}$ then there exists $\rho, \sigma$  such that $\Phi = \Phi', c:!(\sigma).\rho, d:\sigma $ and  $\judgement{\Gamma}{\Theta}{P}{\Phi', c:\rho}{\Delta}$;
 
 \item \label{types4} if $\judgement{\Gamma}{\Theta}{\rec{X:\type{\Phi}{\Delta}}{P}}{\Phi}{\Delta}$ then  $\judgement{\Gamma}{\Theta, X:\type{\Phi}{\Delta}}{P}{\Phi}{\Delta}$;
 \item \label{types5} if $\judgement{\Gamma}{\Theta}{\ifte{e}{P}{Q}}{\Phi}{\Delta}$ then $\judgement{\Gamma}{\Theta}{P}{\Phi}{\Delta}$,  $\judgement{\Gamma}{\Theta}{Q}{\Phi}{\Delta}$ and $\Gamma \vdash e:\mathsf{bool} $;
  \item \label{types6} if $\judgebis{\env{\Gamma}{\Theta}}{\component{l}{n}{\Delta}{P} }{ \type{\Phi}{\Delta}}$ then $\judgement{\Gamma}{\Theta}{P}{\Phi}{\Delta}$ and $n = \#\{c \mid c:\omega \in \Phi\}$;
   \item \label{types7} if $\judgebis{\env{\Gamma}{\Theta}}{\updated{l}{X}{\Delta_1}{\Delta_2}{U}}{\type{\emptyset}{ \emptyset}}$ then $\judgebis{\env{\Gamma}{\Theta,\mathsf{X}:\type{\emptyset}{\Delta_1}}}{ U}{\type{\emptyset}{ \Delta_2 }}$;
   \item \label{types8} if $\judgebis{\env{\Gamma}{\Theta}}{\nopen{a}{c:\rho}.P}{ \type{\Phi}{\Delta,\rho}}$ then $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi, c:\rho}{ \Delta}}$;
   \item \label{types9} if $\judgebis{\env{\Gamma}{\Theta}}{ \close{c}.P}{ \type{\Phi}{ \Delta}}$ then there exists $\Phi'$ with $c\notin \dom{\Phi'} $ such that $\Phi = \Phi', c:\epsilon$ and $\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\Phi}{\Delta}}$;
   \item \label{types10} if $\judgement{\Gamma}{\Theta}{\restr{c}{P}}{\Phi}{\Delta}$ and $c\notin \dom{\Phi}$ then $\judgement{\Gamma}{\Theta}{P}{\Phi}{\Delta}$;
   \item \label{types11} if $\judgebis{\env{\Gamma}{\Theta}} {\restr{c}{P}}{\type{\Phi, c:\bot}{ \Delta}}$ then $\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\Phi, c:\bot }{ \Delta}}$;
   \item \label{types12} if $\judgebis{\env{\Gamma}{\Theta}}{\branch{c}{n:P \dots n:P}}{\type{ \Phi}{ \Delta}}$ then there exists  $\Phi'$ such that $\Phi= \Phi', c:\&\{n_1:\rho_1 \vee \dots \vee n_k:\rho_k \}$ and $\judgebis{\env{\Gamma}{\Theta}}{P_i}{\type{\Phi', c:\rho_i}{ \Delta}}$;
   \item \label{types13} if $\judgebis{\env{\Gamma}{\Theta}}{\select{c}{n_i}.P}{\type{\Phi}{\Delta}}$ then there exists  $\Phi'$ such that $\Phi= \Phi', \oplus\{n_1:\rho_1 \vee \dots \vee n_k:\rho_k$ and $\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\Phi, c:\rho_i}{ \Delta}}$.
\end{enumerate}
\end{lemma}

The third lemma allows the introduction of contexts.  It follows  by induction on the sstructure  of the context using  Lemma \ref{lem:types}.
\begin{lemma}\label{lem:context}
Given a process $P$ and a context $C$, if $\judgement{\Gamma}{\Theta}{C[P]}{\Phi}{\Delta}$ then there exists $\Gamma', \Theta', \Phi', \Delta'$ such that $\judgement{\Gamma'}{\Theta'}{P}{\Phi'}{\Delta'}$.
\end{lemma}

The first theorem we prove allows to consider processes up to structural congruence.

\begin{theorem}[Subject congruence] \label{th:congr}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}}$ and $P \equiv Q$ then $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\Phi}{\Delta}}$.
\end{theorem}
\begin{proof}
The proof proceeds by a case analysis on the structural rule applied to obtain the congruence. 
\end{proof}


Finally, we can prove our main results:
\begin{theorem}[Theorem \ref{th:subred} Subject reduction]
If $$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}}$$ and $P \pired Q$ then one of the following holds:\begin{enumerate}
 \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta}}$;
  \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta'}}$ for some $\Delta'$
  \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi, c:\bot}{\Delta\ominus\{\rho, \overline{\rho}\}}}$ for some $\rho$;
\end{enumerate}
\end{theorem}
\begin{proof}
The proof proceeds by a case analysis on the rule applied for the reduction. Lemma \ref{lem:context} allows us to consider  only the partners involved in the reduction regardless of the contexts where those process appear.
\begin{description}
   \item [Case \rulename{r:I/O}]
We have that $P \equiv \inC{c}{\tilde{x}}.P_1 \parallel \outC{c}{\tilde{e}}.P_2$ and  $$\judgebis{\env{\Gamma}{\Theta}}{\inC{c}{\tilde{x}}.P_1 \parallel \outC{c}{\tilde{e}}.P_2}{ \type{\Phi', c:\bot}{\Delta}}$$ 
where $\Phi = \Phi', c:\bot$.

For Lemma \ref{lem:types}(\ref{types1}) there exists $\Phi_1, \Phi_2, \Delta_1$ and $\Delta_2$ such that $\Delta = \Delta_1 \uplus \Delta_2$, $$\Phi', c:\bot = \Phi_1, c:?(\tilde{\capab}).\rho \bowtie \Phi_2, c:!(\tilde{\capab}).\overline{\rho} $$ for some $\rho$ and 
\begin{enumerate}
 \item $\judgement{\Gamma}{\Theta}{\inC{c}{\tilde{x}}.P_1}{\Phi_1,c:?(\tilde{\capab}).\rho}{\Delta_1} $
 \item $\judgement{\Gamma}{\Theta}{\outC{c}{\tilde{e}}.P_2}{\Phi_2,c:!(\tilde{\capab}).\overline{\rho}}{\Delta_2} $
\end{enumerate}
Then from Lemma \ref{lem:types}(\ref{types2} and \ref{types3}) it follows
$\judgement{\Gamma,\tilde{x}:\tilde{\capab}}{\Theta}{P_1}{\Phi_1,c:\rho}{\Delta_1} \text{ and } \judgebis{\env{\Gamma}{\Theta}}{ P_2}{\Phi_2,c:\overline{\rho}} $
with $\Gamma \vdash \tilde{e}:\tilde{\capab}$.
Thus by Lemma \ref{lem:substitution}(2) and by using typing rule \rulename{Par}  we can conclude $$\env{\Gamma}{\Theta} \vdash P_1\sub{\tilde{e}}{\tilde{x}} \parallel P_2: \type{\Phi}{\Delta} .$$

   \item [Case \rulename{r:Pass}]
We have that $P \equiv \catch{c}{d}.P_1 \parallel \throw{c}{d}.P_2$ and  $$\judgebis{\env{\Gamma}{\Theta}}{\catch{c}{d}.P_1 \parallel \throw{c}{d}.P_2}{ \type{\Phi', c:\bot, d:\sigma}{\Delta}}$$ 
where $\Phi = \Phi', c:\bot, d:\sigma$.

For Lemma \ref{lem:types}(\ref{types1}) there exists $\Phi_1, \Phi_2, \Delta_1$ and $\Delta_2$ such that $\Delta = \Delta_1 \uplus \Delta_2$, $$\Phi', c:\bot = \Phi_1, c:?(\sigma).\rho \bowtie \Phi_2, c:!(\sigma).\overline{\rho},d:\sigma $$ for some $\rho$ and 
\begin{enumerate}
 \item $\judgement{\Gamma}{\Theta}{\catch{c}{d}.P_1}{\Phi_1,c:?(\sigma).\rho}{\Delta_1} $
 \item $\judgement{\Gamma}{\Theta}{\throw{c}{d}.P_2}{\Phi_2,c:!(\sigma).\overline{\rho}, d:\sigma}{\Delta_2} $
\end{enumerate}
Then from Lemma \ref{lem:types}(\ref{typesdelin} and \ref{typesdelout}) it follows
$\judgement{\Gamma}{\Theta}{P_1}{\Phi_1,c:\rho, d:\sigma}{\Delta_1} \text{ and } \judgebis{\env{\Gamma}{\Theta}}{ P_2}{\Phi_2,c:\overline{\rho}} $.
Thus by using typing rule \rulename{Par}  we can conclude $$\env{\Gamma}{\Theta} \vdash P_1  \parallel P_2: \type{\Phi}{\Delta} .$$


\item[Case \rulename{r:Rec}] We have that $P \equiv \rec{X:\type{\Phi}{\Delta}}{P'}$.
For Lemma \ref{lem:types}(\ref{types4}) we have  $\judgement{\Gamma}{\Theta, X:\type{\Phi}{\Delta}}{P}{\Phi}{\Delta} $.  
Now from Lemma \ref{lem:substitution}(3) we have $\judgement{\Gamma}{\Theta}{P\sub{\rec{X:\type{\Phi}{\Delta}}{P}}{X}]}{\Phi}{\Delta}$ thus concluding this case.



\item[Cases \rulename{r:IfTr} and \rulename{r:IfFa}] Follow from Lemma \ref{lem:types}(\ref{types5}).

\item[Case \rulename{r:Upd}] We have $P \equiv \component{l}{0}{\Delta}{P'} \parallel \updated{l}{X}{\Delta}{\Delta'}{U}$ and $\judgebis{\env{\Gamma}{\Theta}}{\component{l}{0}{\Delta}{P'} \parallel \updated{l}{X}{\Delta}{\Delta'}{U}}{ \type{\emptyset}{\Delta}}$
For Lemma \ref{lem:types}(\ref{types1}, \ref{types6} and \ref{types7}) we have that 
$\judgement{\Gamma}{\Theta}{P'}{\emptyset}{\Delta} $ and  $\judgebis{\env{\Gamma}{\Theta,\mathsf{X}:\type{\emptyset}{\Delta}}}{ U}{\type{\emptyset}{ \Delta'}}$. By Lemma \ref{lem:substitution} (4) we obtain $\judgement{\Gamma}{\Theta}{ U\sub{P'}{\mathsf{X}}}{\emptyset}{\Delta'}$. Thus concluding 
$$\judgement{\Gamma}{\Theta}{U\sub{P_1}{\mathsf{X}} \parallel \nil}{\emptyset}{\Delta'} .$$


	\item[Case \rulename{r:Open}]
We have that $P \equiv \nopen{a}{c:\rho}.P_1 \parallel \open{a}{d:\overline{\rho}}.P_2$. 
From Lemma \ref{lem:types}(\ref{types1} and \ref{types8}) we have that there exists $\Phi_1, \Phi_2, \Delta_1$ and $\Delta_2$ such that $\Phi = \Phi_1,  \bowtie \Phi_2$,  $\Delta = \Delta_1 \uplus \Delta_2$, 
$\judgement{\Gamma}{\Theta}{P_1}{\Phi_1, c:\rho}{\Delta_1 \ominus \rho} $ and  $\judgement{\Gamma}{\Theta}{P_2}{\Phi_2, \overline{\rho}}{\Delta_2 \ominus \overline{rho}}$. 

Now from Lemma \ref{lem:substitution} (1) $\judgement{\Gamma}{\Theta}{P_1\sub{c'}{c}}{\Phi_1,c':\rho}{\Delta_1 \ominus \rho} \text{ and } \judgement{\Gamma}{\Theta}{ P_2\sub{c'}{d}}{\Phi_2,c':\overline{\rho}}{\Delta_2 \ominus \overline{\rho}}$.

By means of typing rule \rulename{Par} we obtain  
$$\judgement{\Gamma}{\Theta}{ P_1\sub{c'}{c} \parallel P_2\sub{c'}{d}}{\Phi,c:\bot}{\Delta \ominus \{\rho, \overline{\rho}\}} $$
and finally by typing rule \rulename{Restr} we can conclude
$\judgement{\Gamma}{\Theta}{\restr{c'}{P_1\sub{c'}{c} \parallel P_2\sub{c'}{d}}}{\Phi, c:\bot}{\Delta \ominus \{\rho, \overline{\rho}\}}$ .

\item[Case \rulename{r:Close}] This case follows the same lines of  \rulename{r:Open} case and uses Lemma \ref{lem:types}(\ref{types9}).

\item[Case \rulename{r:Branch}] This case is similar to  previous \rulename{r:I/O} case where Lemma \ref{lem:types}(\ref{types12} and \ref{types13}) is used.




\item[Case \rulename{r:Str}] Follows by theorem \ref{th:congr}.

\item[Case \rulename{r:Res}] Follows by induction on the derivation tree and by using Lemma \ref{lem:types}(\ref{types10} and \ref{types11}).
\end{description}
\end{proof}
